COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	ideas[s84,jmc]		circum vs. default logic
C00005 ENDMK
C⊗;
ideas[s84,jmc]		circum vs. default logic

default logic can infer consistency of arith, but disj. and circum
is more nearly effective

takasu

1. We infer that something is best, because it is consistent that it
the best.  Circumscribe  better(x,candidate).

2. The bolder conjectures are made by circumscribing w/r subsets
of the available facts.

apr 23
What about a program that investigated what words and phrases a person used
frequently and then offered a set of macros that abbreviated them?
One cculd imagine putting E or some other editor in a collect mode
for the purpose of accumulating the statistics.

apr 28
Can we get termination of Ackermann function by a simple recursion
on a higher type?  What about the Goodstein function?  Perhaps it
requires recursion of some transfinite type.  What about higher
combinators?  Is there some generalization of  mapcar  which is
a combinator?

may 21
Introduce Q as a parameter only parenthetically.

Parametrization of Boolean functions.  Investigate which Boolean
functions don't split into Boolean functions of functions of
disjoint subsets of the variables.  Partial splitting as in
incompletely reducible representations.  The counting functions,
e.g. 3 of p q r s t  provide examples indecomposability.

Partial models and their relation to JK's obvious.  Proving
∃x∀y(Px ⊃ Py) involves disproving Px ∧ ¬Pfx.  This is not "obvious",
but disproving  Px ∧ ¬Pfx ∧ Pu ∧ ¬Pgu  is "obvious".

In propositional circumscription, we really can just minimize
Axiom ⊃ E  rather than minimize  E  holding Axiom.